#include "PDTCodeGraph.h"
#include "PDTSpecCheck.h"
#include "PDTCheckSpec.h"

#include "PDTNode.h"


extern PDTCodeGraph * mini_main(const string & file);

int 
specCheckMain(const string & file, const string & func, const string & spec)
{
	PDTCodeGraph * cg = mini_main(file);

try{    
    PDTCheckSpec check(*cg, func, spec);
    check.checkPrePost();
} catch ( PDTException & e){
    cerr << e.str() << endl;
} 

try{    
    PDTCheckSpec check(*cg, func, spec);
    check.check();
} catch ( PDTException & e){
    cerr << e.str() << endl;
} 
return 0;
    
    PDTSpecCheck check(cg);

     //check.checkGood("LinearSearch", 0);                        //Check the conditions by themselves - only good behaviors
     //check.checkBad("LinearSearch", 0);                         //Check the conditions by themselves - only bad behaviors
     //check.checkAllGood("LinearSearch");						 //Check the conditions by themselves - all good behaviors
     //check.checkAllBad("LinearSearch");						 //Check the conditions by themselves - all bad behaviors

     //vector <PDTIntRange*> ranges;
     //vector <PDTVar*> variables;
     //check.buildRanges("LinearSearch", ranges, variables);      //Build Ranges for the inputs
     //check.getFunctionCode("LinearSearch");  	 				 //Get the program code
     //check.checkWithCode("LinearSearch");				 //Check all good behaviors while involving the program code
     //check.buildRangesAll("selectionSort", ranges, variables);
     check.check(func,spec);
     return 0;


     vector <PDTNode*> noParents;
     stringstream ss(stringstream::in | stringstream::out);
     //ss<<"==========="<<endl;


     for (unsigned int i = 0; i < cg->nodes.size(); i++)
	 {
		PDTNode * node = cg->nodes[i];
		//if (node->getParents().size() == 0)
		//cout<<"is? "<<node->isIfElse()<<endl;
		if (node->isFunctionDec())
		{
			//node->clone(*cg);
			//node->toString(ss);ss<<endl;
			//ss<<node->isForall()<<endl;
			break;
		}
	 }

     for (unsigned int i = 0; i < cg->nodes.size(); i++)
     {
         PDTNode * node = cg->nodes[i];
         //if (node->getParents().size() == 0)
         //{
         //cout<<"is? "<<node->isIfElse()<<endl;
         if (node->isFunctionDec())
         {	//node->clone(*cg);
             //node->toString(ss);ss<<endl;
             //ss<<node->isForall()<<endl;
             break;}
             //}
     }

	for (unsigned int i = 0; i < cg->nodes.size(); i++)
    {
        PDTNode * node = cg->nodes[i];
        if (node->getParents().size() == 0)
        {
            //if (!(node->isFunctionDec()))
            //{
            //node->toString(ss);
            //ss<<" "<<i<<endl;
            noParents.push_back(node);
            //node->eval(*cg);
            //}
        }
    }

    for (unsigned int i = 0; i < noParents.size(); i++) {
        PDTNode * node = noParents[i];
        if (node->getParents().size() == 0)
        {
            //if (!(node->isFunctionDec()))
            //{
            ss<<i<<" ";
            node->toString(ss);
            ss<<endl;
            //noParents.push_back(node);
            //node->eval(*cg);
            //}
        }
    }
     cout<<ss.str()<<endl;

     /*cout<<"PRITING ALL VARIABLES: "<<endl;
     for (unsigned int i = 0; i < cg->nodes.size(); i++)
	 {
		PDTNode * node = cg->nodes[i];
			if (node->isVar())
			{
				cout<<((PDTNumVar*)node)->getName()<<endl;
			}

	 }*/

     /*for (unsigned int i = 0; i < noParents.size(); i++)
	 {
		PDTNode * node = noParents[i];
		if (node->getParents().size() == 0)
		{
			if (node->isFunctionCall() || node->isAssign() )
				node->eval(*cg);

		}
	 }*/
     //noParents[0]->clone(*cg);
     noParents[0]->eval(*cg);
     noParents[3]->eval(*cg);
     //noParents[5]->eval(*cg);
     //noParents[6]->eval(*cg);
     //noParents[7]->eval(*cg);
     //noParents[8]->eval(*cg);
     //noParents[9]->eval(*cg);

     ///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////

     return 0;
 }
